We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic proofs and, by the Curry-Howard correspondence, into the domain of typed functional programs. We begin by reviewing well-known homomorphic encryption schemes for arithmetic operations, and then discuss the adaptation of similar concepts to support logical inference steps in intuitionistic logic. Key to our construction are polynomial functors and Bounded Natural Functors (BNFs), which serve as a categorical substrate on which logic formulas and proofs are represented and manipulated. We outline a complexity-theoretic hardness assumption -- the BNF Distinguishing Problem, constructed via a reduction from Subgraph Isomorphism, providing a foundation for cryptographic security. Finally, we describe how these methods can homomorphically encode the execution of total, dependently typed functional programs, and outline strategies for making the approach potentially efficient, including software optimizations and hardware acceleration.

A definition of what counts as an explanation of mathematical statement, and when one explanation is better than another, is given. Since all mathematical facts must be true in all causal models, and hence known by an agent, mathematical facts cannot be part of an explanation (under the standard notion of explanation). This problem is solved using impossible possible worlds.

We consider a swarm of mobile robots evolving in a bidimensional Euclidean space. We study a variant of the crash-tolerant gathering problem: if no robot crashes, robots have to meet at the same arbitrary location, not known beforehand, in finite time; if one or several robots crash at the same location, the remaining correct robots gather at the crash location to rescue them. Motivated by impossibility results in the semi-synchronous setting, we present the first solution to the problem for the fully synchronous setting that operates in the vanilla Look-Compute-Move model with no additional hypotheses: robots are oblivious, disoriented, have no multiplicity detection capacity, and may start from arbitrary positions (including those with multiplicity points). We furthermore show that robots gather in a time that is proportional to the initial maximum distance between robots.

We implement and interpret various supervised learning experiments involving real quadratic fields with class numbers 1, 2 and 3. We quantify the relative difficulties in separating class numbers of matching/different parity from a data-scientific perspective, apply the methodology of feature analysis and principal component analysis, and use symbolic classification to develop machine-learned formulas for class numbers 1, 2 and 3 that apply to our dataset.

Differential privacy is a formal algorithmic guarantee that no single input has a large effect on the output of a computation. Since its introduction [13] over a decade ago, a rich line of work has made differential privacy a compelling privacy guarantee (see Dwork et al. [14] and Vadhan [26] for surveys), and deployments of differential privacy now exist at many organizations, including Apple [3], Google [6, 15], Microsoft [11], Mozilla [4], and the US Census Bureau [1, 22]. Much recent attention, including almost all industrial deployments, has focused on a stronger variant of differential privacy called local differential privacy [16, 21, 27]. In the local model private data is distributed across many users, and each user privatizes their data before the data is collected by an analyst. Thus, as any locally differentially private computation runs on already-privatized data, data contributors need not worry about compromised data analysts or insecure communication channels.In contrast, (global) differential privacy assumes that the data analyst has trusted access to the unprivatized data. As a result, under global differential privacy any violation of this trust may lead to serious privacy loss for the users contributing the data.

We identify three classes of four-state paraconsistent logics according to their different approaches towards the disjunctive syllogism, and investigate three representatives of these approaches: Quasi-classical logic, which always accepts this principle, Belnap's logic, that rejects the disjunctive syllogism altogether, and a logic of inconsistency minimization that restricts its application to consistent fragments only. These logics are defined in a syntactic and a semantic style, which are linked by a simple transformation. It is shown that the three formalisms accommodate knowledge minimization, and that the most liberal formalism towards the disjunctive syllogism is also the strongest among the three, while the most cautious logic is the weakest one.